;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface IResize
  (sig calcBilinear (Q11Val Q21Val Q12Val Q22Val x1 x2 y1 y2 x y))
  (sig calcAndInsertPix (newTree Q11 Q21 Q12 Q22 x1 x2 y1 y2 x y))
  (sig validCord (nextX nextY beginWidth height))
  (sig calcNextY (y endOfX))
  (sig calcNextX (x x1 x2))
  (sig bilinearInterpolateSquare (newTree Q11 Q21 Q12 Q22 x1 x2 y1 y2 x y))
  (sig getListOfMatchingRowPix (listOfOldTreeElementsAndNewLocationPairs rowNum returnList partialList))
  (sig insertOldElements (newTree oldTree returnList x y oldTreeWidth oldTreeHeight percentIncreaseW percentIncreaseH))
  (sig interPolateBottomRightCorner (treeWithRightSectionCalculated topLeftCorner defaultXIncrement defaultYIncrement))
  (sig interPolateRightSection (treeWithBottomSectionCalculated farRightColumn defaultXIncrement defaultYIncrement))
  (sig interPolateBottomSection (treeWithMainPartCalculated bottomRow defaultXIncrement defaultYIncrement bottomLeftElement topLeftElement))
  (sig interPolateRowMainSection (newTree mainRow secondRow defaultXIncrement defaultYIncrement bottomLeftElement topLeftElement))
  (sig interPolateMainSection (newTree listOfListsOfMatchingRowPixels defaultXIncrement defaultYIncrement))
  (sig getFarRightColumn (listOfListsOfMatchingRowPixels returnList))
  (sig createNewTree (tree newTreeWidth newTreeHeight oldTreeWidth oldTreeHeight percentIncreaseW percentIncreaseH))
  (sig calcPercentIncrease (currentTreeWidth currentTreeHeight newWidth newHeight))
  (sig resizeProportional (tree currentTreeWidth currentTreeHeight newWidth newHeight))
  (sig getRGBAverage (oldTreePixelVals listLength rSum gSum bSum))
  (sig getPixelVals (pixelCoordinates oldTree returnList))
  (sig validCordShrink (nextX nextY beginWidth height))
  (sig calcNextYShrink (y endOfX))
  (sig calcNextXShrink (x x1 x2))
  (sig getCoordinates (returnList minBoxW minBoxH maxBoxW maxBoxH x y))
  (sig calcCoordinates (x y pixRepSquareWidth pixRepSquareHeight centerValW centerValH newWidth newHeight))
  (sig insertCalculatedElements (newTree oldTree x y newWidth newHeight pixRepSquareWidth pixRepSquareHeight centerValW centerValH))
  (sig createNewTreeShrink (oldTree newWidth newHeight pixRepSquareWidth pixRepSquareHeight centerValW centerValH))
  (sig shrinkResize (tree currentTreeWidth currentTreeHeight newWidth newHeight))
  (sig checkShrinkOrExpand (tree currentTreeWidth currentTreeHeight newWidth newHeight))
  (sig mainResize (tree args))
  
  (con validResize
       (let* ((result (mainResize x y)))
         (and (tree? (car result)) (listp (cadr result))))))